FDL - Nuprl Lemma : sq_stable__monot

Nuprl Lemma : sq_stable__monot

T:Type, R:(T

T

), f:(T

T). (

x, y:T. SqStable(R(x,y)))

SqStable(monot(T;x,y.R(x,y);f))

Up gen algebra 1

Definitions of Statement monot(T;x,y.R(x;y);f)

Definitions x. t(x), t T, monot(T;x,y.R(x;y);f), x(s1,s2), P Q, , x:A. B(x), x(s)

Lemmas sq stable wf, sq stable implies, sq stable all